; <lemma>
;  <title>BoschSwitch.3</title>
;  <origin>BoschSwitch | m1 | Tick/inv1/INV</origin>
(benchmark boschswitch_3
;  <theories>
;    <theory name="linear_order_int"/>
;  </theories>
  :logic QF_LIA
;  <typenv>
;    <variable name="clk" type="INTEGER"/>
;  </typenv>
  :extrafuns (
	       (clk Int) 
	       )
  :extramacros (
		 (Nat
		  (lambda (?i Int) . (<= 0 ?i)))
		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 )
;  <hypothesis needed="true">clk : NATURAL</hypothesis>
  :assumption (in clk Nat)
;  <goal>clk+1 : NATURAL</goal>
  :formula
  (not
      (in (+ clk 1) Nat)
    )
)
; </lemma>
